package Transformer.CounterExample;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.util.ArrayList;
import java.util.List;
import java.util.regex.Pattern;

public class CounterExampleGeneration {
	
	// This pattern is used for identifying the counterexample
	public static final String COUNTEREXAMPLE_PATTERN = "([ \t]*)([0-9]*):([ \t]*)proc([ \t]*)1(.*)line([ \t]*)([0-9]*)([ \t]*)\"(.*)\"([ \t]*)\\(state([ \t]*)([0-9]*)\\)([ \t]*)\\[(.*)\\]";
	// These patterns are used for extracting the piece of code containing the counterexample 
	public static final String SPLITTING_COUNTEREXAMPLE_PATTERN = "\"(.*)\"([ \t]*)\\(state([ \t]*)([0-9]*)\\)";
	public static final String REPLACED_COUNTEREXAMPLE_PATTERN = "([ \t]*)([0-9]*):([ \t]*)proc([ \t]*)1(.*)line";
	// This pattern is used for identifying the local variables
	public static final String LOCAL_VAR_PATTERN = "([ \t]+)(bool|unsigned[ ]char|short[ ]int|int)([ \t]+)([a-zA-Z_][a-zA-Z_0-9]*):([ \t]+)([-]?)([0-9]*)";
	// These patterns are used for extracting the local variables' name and value
	public static final String SPLITTING_VAR_PATTERN = ":([ \t]+)";
	public static final String REPLACED_VAR_PATTERN = "([ \t]+)(bool|unsigned[ ]char|short[ ]int|int)([ \t]+)";
	public static final String EMPTY_STRING = "";
	public static final String LEFTSQURBRK = "[";
	public static final String RIGHTSQURBRK = "]";
	public static final String LEFTPAR = "(";
	public static final String RIGHTPAR = ")";
	
	// This variable holds the counterexample file
	private File counterexample;
	
	/**
	 * @param counterexample
	 */
	public CounterExampleGeneration(File counterexample) {
		super();
		this.counterexample = counterexample;
	}

	/**
	 * This function parses the counterexample generated by SPIN and
	 * then returns the error path indicating why and where the error occurred.
	 * @param ce
	 */
	public List<Entry> GenerateCounterExample () {
		
		List<Entry> errorPath = new ArrayList<Entry>();
		
		try {
			BufferedReader reader = new BufferedReader(new FileReader(counterexample));
			while (true) {
				String line = reader.readLine();
				if (line != null) {
					if (Pattern.matches(COUNTEREXAMPLE_PATTERN, line)) {
						errorPath.add(getEntry(line));
					}
				} else {
					// close the file
					reader.close();
					// get out of the loop
					break;
				}
			}
		} catch (IOException except) {
			// TODO handle the IO Exception here
		}
		
		return errorPath;
	}
	
	private Entry getEntry (String line) {
		Entry entry = new Entry();
		String[] codeSegments = line.split(SPLITTING_COUNTEREXAMPLE_PATTERN);
		// Get the line from the counterexample
		codeSegments[0] = codeSegments[0].replaceFirst(REPLACED_COUNTEREXAMPLE_PATTERN, EMPTY_STRING);
		entry.setLine(Integer.parseInt(codeSegments[0].trim()));
		// Get the code from the counterexample
		codeSegments[1] = codeSegments[1].trim();
		// Eliminate [ and ] around the code
		if (codeSegments[1].startsWith(LEFTSQURBRK) && codeSegments[1].endsWith(RIGHTSQURBRK)) {
			codeSegments[1] = codeSegments[1].substring(1, codeSegments[1].length() - 1);
		}
		// Eliminate ( and ) around the code
		while (codeSegments[1].startsWith(LEFTPAR) && codeSegments[1].endsWith(RIGHTPAR)) {
			codeSegments[1] = codeSegments[1].substring(1, codeSegments[1].length() - 1);
		}
		entry.setCode(codeSegments[1]);
		
		return entry;
	}
	
	public List<Variable> GetListOfVariables (List<String> listOfVarNames) {
		
		List<Variable> lst = new ArrayList<Variable>();
		
		if (listOfVarNames != null) {
			List<Variable> localVars = GetLocalVars();
			for (int i = 0; i < listOfVarNames.size(); i++) {
				for (int j = 0; j < localVars.size(); j ++) {
					if (localVars.get(j).getVariableName().equals(listOfVarNames.get(i))) {
						lst.add(localVars.get(j));
						break;
					}
				}
			}
		}
		
		return lst;
	}
	
	private List<Variable> GetLocalVars () {
		
		List<Variable> lst = new ArrayList<Variable>();
		
		try {
			BufferedReader reader = new BufferedReader(new FileReader(counterexample));
			while (true) {
				String line = reader.readLine();
				if (line != null) {
					if (Pattern.matches(LOCAL_VAR_PATTERN, line)) {
						Variable var = new Variable();
						String[] codeSegments = line.split(SPLITTING_VAR_PATTERN);
						// Get the variable's name
						codeSegments[0] = codeSegments[0].replaceFirst(REPLACED_VAR_PATTERN, EMPTY_STRING);
						var.setVariableName(codeSegments[0].trim());
						// Get the variable's value
						var.setVariableValue(codeSegments[1].trim());
						lst.add(var);
					}
				} else {
					// close the file
					reader.close();
					// get out of the loop
					break;
				}
			}
		} catch (IOException except) {
			// TODO handle the IO Exception here
		}
		
		return lst;
	}
	
	/*public static void main(String[] args) {
		CounterExampleGeneration generator = new CounterExampleGeneration(new File("C:/cygwin/home/Administrator/tests/test/result.txt"));
		List<String> temp = new ArrayList<String>();
		temp.add("obtainedResult");
		temp.add("desiredResult");
		List<Variable> lst = generator.GetListOfVariables(temp);
		for (int i = 0; i < lst.size(); ++i) {
			System.out.print(lst.get(i).getVariableName() + "\t");
			System.out.println(lst.get(i).getVariableValue());
		}
		
//		CounterExampleGeneration generator = new CounterExampleGeneration(new File("C:/cygwin/home/Administrator/tests/test/result.txt"));
//		List<Entry> lst = generator.GenerateCounterExample();
//		for (int i = 0; i < lst.size(); ++i) {
//			System.out.print(lst.get(i).getLine() + "\t");
//			System.out.println(lst.get(i).getCode());
//		}
	}*/
}
